\begin{tabbing}
es{-}ble\{i:l\}(${\it es}$;$e$;${\it e'}$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=case TERMOF\{decidable\_\_es{-}le:ObjectId, 1:l, i:l\}(${\it es}$,${\it e'}$,$e$)\+
\\[0ex]o\=f inl($x$) =$>$ tt\+
\\[0ex]$\mid$ inr($x$) =$>$ ff
\-\-
\end{tabbing}